-
Notifications
You must be signed in to change notification settings - Fork 193
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
tensor product distributes over direct sum #2079
tensor product distributes over direct sum #2079
Conversation
<!-- ps-id: eb39fcb0-37ae-4e35-a619-c99f476f071a --> Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM after the minor cleanups I just indicated.
Signed-off-by: Ali Caglayan <[email protected]>
FTR we will eventually prove a more general version of this lemma for indexed products/biproducts but this will probably end up requiring funext if we go through the adjunction route. So its good to have this simple case explicitly written out. |
We show that tensor products distribute over sums.